T:Type, eq:EqDecider(T), f:(TT). retraction(T;f)  (x:T. f**(x)  T) 

latex

Definitions

x:A  B(x), x:A. B(x), retraction(T;f), t  T, x:AB(x), x:A. B(x), f**(x), s = t, strong-subtype(A;B), P  Q, Type, EqDecider(T), left + right, P  Q, {x:A| B(x)} , , |g|, S  T, , n - m, Outcome, False, A, A  B, i  j , -n, Void, #$n, f(a), n+m, a < b, , P & Q, P  Q, , b, eqof(d), p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, , x f y, =, a < b, =, =, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), b, p  q, p  q, p q, ff, tt, Unit, P  Q

Lemmas

iff wf, rev implies wf, deq property, eqtt to assert, assert wf, not wf, bool wf, iff transitivity, eqff to assert, assert of bnot, ge wf, nat properties, nat ind tp, nat wf, deq wf, retraction wf, member wf